COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input macro[1,mps]
C00015 ENDMK
C⊗;
\input macro[1,mps]
\input macrwf[1,mps]
\magnification\magstephalf
\baselineskip 14pt
\leftline{\sevenrm A106H.Tex[106,rwf]\today}
\leftline{\copyright\sevenrm Robert W. Floyd, November 6, 1989}
\leftline{\sevenrm Unpublished draft}
\bigskip
{\bf Designing Programs Around Invariants}

I want to compute $a↑b$, for arbitrary $a$ and arbitrary natural number $b$.
There is an obvious method:  start with 1, and multiply by $a$, $b$ times.
This works even when $b$ is zero.  Here is the algorithm:

{\obeylines\sfcode`;=3000\parskip=0pt\parindent=20pt
$z\leftarrow 1$;$\, x\leftarrow a$;$\, y\leftarrow b$;
{\bf while} $y \not= 0$ {\bf do}
\quad {\bf begin}
\quad $z \leftarrow z \cdot z$
\quad $y \leftarrow y - 1$
\quad {\bf end}
$\{$Result is  $z\}$\par}

At the beginning of each iteration, the final value of $z$ can be predicted
to be $z\cdot x↑y$, so $z\cdot x↑y$ is an invariant expression.  Its initial
value is $1\cdot a↑b$, so $z\cdot x↑y = a↑b$ is an invariant assertion.
When $y=0$, it simplifies to $z = a↑b$.  Any operation that preserves the
invariant and eventually makes $y=0$  can be used in this algorithm.  We can also
square $x$ and halve $y$ whenever $y$ is even; this approaches $y=0$ much
faster:

{\obeylines\sfcode`;=3000\parskip=0pt\parindent=20pt
$z\leftarrow 1$; $x\leftarrow a$; $y\leftarrow b$;
{\bf while} $y \not= 0$ {\bf do}
\quad {\bf if} $y$ {\rm is even}
\quad {\bf then}
\qquad {\bf begin}
\qquad $x\leftarrow x\cdot x$;
\qquad $y\leftarrow y/2$
\qquad {\bf end}
\quad {\bf else}
\qquad {\bf begin}
\qquad $z\leftarrow z\cdot x$;
\qquad $y\leftarrow y-1$
\qquad {\bf end}
$\{$Result is $z\}$\par}

\noindent The invariants are as before, but the algorithm requires no 
more than $2\,\log↓2 b$ multiplications.

This pattern is a common way to get a correct and efficient algorithm:

\item{(1)}  Find a simple algorithm that is clearly correct.
\item {(2)}  Determine its invariants, especially the final values of all
variables.
\item{(3)}  Look for operations that preserve the invariant, but approach a
final result more quickly.

The invariant assertion $z\cdot x↑y = a↑b$ has several desirable properties.

\item{(1)}  It is easy to establish.  By inspection, setting $z=1$, $x=a$,
$y=b$ is enough.
\item{(2)}  There are several operations that preserve it, suggested by

\halign{\qquad\qquad#\hfil&\qquad#\hfil\cr
\null \phantom{=}$z\cdot x↑y$\cr
\null = $(z\cdot x)\cdot x↑{y-1}$& $z\leftarrow z\cdot x, \,y\leftarrow y-1$\cr
\null = $z\cdot (x↑2)↑{y/2}$& $x\leftarrow x\cdot x, \,y\leftarrow y/2$\cr
\null = $(z/x)\cdot x↑{y+1}$& $z\leftarrow z/x, \,y\leftarrow y+1$\cr}

\item{(3)}  There are conditions under which the invariant assertion announces
the correct result.  Here, making $x = 1$ or $y = 0$ simplifies the assertion
to $z = a↑b$.  Though there are no obvious ways to make $x=1$, it is easy
to make $y=0$.

A similar invariant expression is $y\,\log↓2 x + z$.  Its value is preserved by
the operations
$$\displaylines{x\leftarrow 2x,\, z\leftarrow z-y\cr
x\leftarrow x/2,\, z\leftarrow z+y\cr
x\leftarrow x\cdot x,\, y\leftarrow y/2\cr}$$
If we want to compute $\log↓2a$, we could use $y\,\log↓2 x + z = \log↓2a$
as an invariant assertion, then try to reach a condition in which
$y\, \log↓2 x=0$, either because
$y=0$ or because $x=1$, so that $z=\log↓2a$.  The invariant assertion is
established by $y\leftarrow 1$, $x\leftarrow a$, $z\leftarrow 0$.

Let's try the approach of forcing $y$ toward zero.  The operation
$$x\leftarrow x\cdot x, \,y\leftarrow y/2$$
makes $y$ approach zero rapidly.  Unfortunately, it doesn't change the value
of $y \,\log↓2 x$; however, $x$ can be kept small (say, between 1 and 2) by the 
other two operations.  If $1 \leq x < 2$, $0 \leq \log↓2 x < 1$, and 
$0 \leq \mid y\, \log↓2 x\mid <\mid y\mid$.  Our strategy will be first to make
$x \geq 1$, then to halve it when $x \geq 2$, and square it otherwise.

The algorithm:

{\obeylines\sfcode`;=3000 \parskip=0pt \parindent=20pt
$\{a > 0\}$
$y\leftarrow 1$, $x\leftarrow a$, $z\leftarrow 0$
$\{y \,\log↓2 x + z = \log↓2 a$, $y > 0\}$
{\bf while} $x < 1$ {\bf do} $\{${\rm operation} 1$\}$
\quad {\bf begin}
\quad $x\leftarrow 2\cdot x$
\quad $z\leftarrow z- y;$
\quad {\bf end}
$\{y \,\log↓2 x + z =\log↓2 a$, $1 \leq x$, $y > 0\};$
{\bf while} $x \geq 2$ {\bf or} $y >$ {\it epsilon} {\bf do}
\quad{\bf if} $x \geq 2$ {\bf then} $\{${\rm operation} 2$\}$
\qquad {\bf begin}
\qquad $x\leftarrow x/2$, $z\leftarrow z + y$
\qquad {\bf end}
\quad {\bf else} $\{${\rm operation} 3$\}$
\qquad {\bf begin}
\qquad $x\leftarrow x\cdot x$, $y\leftarrow y/2$
\qquad {\bf end}
$\{y \,\log↓2 x + z = \log↓2 a, 1 \leq x < 2, 0 < y \leq {\it epsilon}\}$

For $a = 10$, {\it epsilon} $= 0.001$ the computation is
\medskip
\halign{\hfil#&\quad#\hfil&\quad#\hfil&\quad#\hfil\cr
&$x$&$y$&$z$\cr
&\hbox to 0pt{\hss 1}0&1&0\cr
$\{2\}$&5&&1\cr
$\{2\}$&2.5&&2\cr
$\{2\}$&1.25&&3\cr
$\{3\}$&1.5625&0.5&\cr
$\{3\}$&2.4414062&0.25&\cr
$\{2\}$&1.2207031&&3.25\cr
$\{3\}$&1.4901160&0.125&\cr
$\{3\}$&2.2204456&0.0625&\cr
$\{2\}$&1.1102228&&3.3125\cr
$\{3\}$&1.2325946&0.03125&\cr
$\{3\}$&1.5192894&0.015625&\cr
$\{3\}$&2.3082402&0.0078125&\cr
$\{2\}$&1.1541201&&3.3203125\cr
$\{3\}$&1.3319932&0.0039063&\cr
$\{3\}$&1.7742058&0.0019532&\cr
$\{3\}$&3.1478062&0.0009766&\cr
$\{2\}$&1.5739031&&3.3212891\cr}}
\medskip
So $\log↓2 10 = 3.321$, $\log↓{10} 2 = {1\over 3.321} = 0.301$.

While the algorithm above is not the way logarithms are commonly calculated, it
could be used to produce log tables by the formula $\log↓b a = \log↓2 a/\log↓2 b$.  
The number of operations is at most $\mid\log↓2 a\mid - 2 \log↓2 {\it epsilon}$.

Suppose in Table A we have entries $A↓1 < A↓2 <\cdots < A↓N$.  We have a value
$X$; we want to find which $A↓i$, if any, is equal to $X$.  We will maintain
the invariant that $A↓L < X \leq A↓R$.  This  invariant may be established by 
$L\leftarrow 0$, $A↓0\leftarrow - \infty$, $R\leftarrow N+1$, 
$A↓R\leftarrow +\infty$.  
The invariant implies $A↓L < A↓R$, so $L < R$.  Since $X\leq A↓R < A↓{R+1}$
the possible locations for $X$ are $L+1$ through $R$, numbering $R-L$.
If $R = L + 1$, there is only one candidate, $A↓R$, and the program leaves
the iteration.  If $L+1 < R$, take $M$ as a value between $L$ and $R$; compare
$X$ to $A↓M$.  If $A↓M < X$, $L\leftarrow M$.  If $X\leq A↓M$, $R\leftarrow M$.
In either case, the invariant is preserved, $R-L$ decreases, and $R-L\geq 1$.
(The algorithm will work when $N=0$.)  After leaving the iteration,
$A↓{R-1} = A↓L < X \leq A↓R < A↓{R+1}$, so $A↓R$ is the only candidate; test
whether $X = A↓R$.  No comparisons to $A↓0$ are ever made, but if $X > A↓N$, it is 
compared to $A↓{N+1}$.
\vfill
\eject
The algorithm:

{\obeylines \sfcode`;=3000\parskip=0pt\parindent=20pt
{\bf Read} $N$;
{\bf Iterate} $i$ from 1 to $N$:
\quad {\bf Read} $A↓i$.
{\bf Set} $A↓{N+1} = + \infty$, $L = 0$, $R = N+1$
$\{A↓L < X \leq A↓R\}$
{\bf while} $L + 1 < R$:
\quad {\bf Begin}
\quad $\{A↓L < X \leq A↓R\}$
\quad{\bf Set} $M = (L+R) {\rm DIV}\, 2 \{{\rm or} = L+1\}$
\quad {\bf If} $A↓M < X$ {\bf then set} $L = M$ {\bf else set} $ R = M$
\quad {\bf End}
$\{R = L+1; A↓{R-1} = A↓L < X \leq A↓R < A↓{R+1}\}$\par}

If $X = A↓R$ then write (X, `at location', R) else write ( X, `not found').

The above algorithm could be designed and tested first in a simple iterative form
where $M=L+1$, then improved in speed by $M=\lfloor (L+R)/2\rfloor$.

{\narrower\smallskip\noindent
{\bf Exercise:}  Adapt the above algorithm to the invariant $A↓L\leq X < A↓R$.
\end